1  /-
  2  Copyright (c) 2019 Zhouhang Zhou. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Zhouhang Zhou
  5  
  6  Show that each Borel measurable function can be approximated,
  7  both pointwise and in L¹ norm, by a sequence of simple functions.
  8  -/
  9  
 10  import measure_theory.l1_space
src         └─────────────────────┘
 11  
 12  noncomputable theory
 13  open lattice set filter topological_space
 14  open_locale classical topological_space
 15  
 16  universes u v
 17  variables {α : Type u} {β : Type v} {ι : Type*}
 18  
 19  namespace measure_theory
 20  open ennreal nat metric
 21  open_locale measure_theory
 22  variables [measure_space α] [normed_group β] [second_countable_topology β]
 23  
 24  local infixr ` →ₛ `:25 := simple_func
 25  lemma simple_func_sequence_tendsto {f : α → β} (hf : measurable f) :
 26    ∃ (F : ℕ → (α →ₛ β)), ∀ x : α, tendsto (λ n, F n x) at_top (𝓝 (f x)) ∧
 27    ∀ n, ∥F n x∥ ≤ ∥f x∥ + ∥f x∥ :=
 28  -- enumerate a countable dense subset {e k} of β
 29  let ⟨D, ⟨D_countable, D_dense⟩⟩ := separable_space.exists_countable_closure_eq_univ β in
 30  let e := enumerate_countable D_countable 0 in
 31  let E := range e in
 32  have E_dense : closure E = univ :=
 33    dense_of_subset_dense (subset_range_enumerate D_countable 0) D_dense,
 34  let A' (N k : ℕ) : set α :=
 35    f ⁻¹' (metric.ball (e k) (1 / (N+1 : ℝ)) \ metric.ball 0 (1 / (N+1 : ℝ))) in
 36  let A N := disjointed (A' N) in
 37  have is_measurable_A' : ∀ {N k}, is_measurable (A' N k) :=
 38    λ N k, hf.preimage $ is_measurable.inter is_measurable_ball $ is_measurable.compl is_measurable_ball,
 39  have is_measurable_A : ∀ {N k}, is_measurable (A N k) :=
 40    λ N, is_measurable.disjointed $ λ k, is_measurable_A',
id                        └────────┘
src                       └────────┘
typ                       └────────┘
 41  have A_subset_A' : ∀ {N k x}, x ∈ A N k → x ∈ A' N k := λ N k, inter_subset_left _ _,
id                                                                  └───────────────┘
src                                                                 └───────────────┘
typ                                                                 └───────────────┘
 42  have dist_ek_fx' : ∀ {x N k}, x ∈ A' N k → (dist (e k) (f x) < 1 / (N+1 : ℝ)) :=
id                                               └──┘
src                                              └──┘
typ                                              └──┘
 43    λ x N k, by { rw [dist_comm], simpa using (λ a b, a) },
src                  └──┘           └──────────┘  └────┘ └┘
typ                  └──┘           └──────────┘  └────┘ └┘
doc                  └──┘           └──────────┘  └────┘ └┘
txt                  └──┘           └──────────┘  └────┘ └┘
par                  └──┘           └──────────┘  └────┘ └┘
pid                    └┘                └────┘  └────┘ 
 44  have dist_ek_fx : ∀ {x N k}, x ∈ A N k → (dist (e k) (f x) < 1 / (N+1 : ℝ)) :=
id                                             └──┘
src                                            └──┘
typ                                            └──┘
 45    λ x N k h, dist_ek_fx' (A_subset_A' h),
 46  have norm_fx' : ∀ {x N k}, x ∈ A' N k → (1 / (N+1 : ℝ)) ≤ ∥f x∥ := λ x N k, by simp [ball_0_eq],
src                                                                                 └────┘         
typ                                                                                 └────┘         
doc                                                                                 └────┘         
txt                                                                                 └────┘         
par                                                                                 └────┘         
pid                                                                                              
 47  have norm_fx : ∀ {x N k}, x ∈ A N k → (1 / (N+1 : ℝ)) ≤ ∥f x∥ := λ x N k h, norm_fx' (A_subset_A' h),
 48  -- construct the desired sequence of simple functions
 49  let M N x := nat.find_greatest (λ M, x ∈ ⋃ k ≤ N, (A M k)) N in
id                └───────────────┘
src               └───────────────┘
typ               └───────────────┘
doc               └───────────────┘
 50  let k N x := nat.find_greatest (λ k, x ∈ A (M N x) k) N in
id                └───────────────┘
src               └───────────────┘
typ               └───────────────┘
doc               └───────────────┘
 51  let F N x := if x ∈ ⋃ M ≤ N, ⋃ k ≤ N, A M k then e (k N x) else 0 in
 52  -- prove properties of the construction above
 53  have k_unique : ∀ {M k k' x},  x ∈ A M k ∧ x ∈ A M k' → k = k' := λ M k k' x h,
 54  begin
 55    by_contradiction k_ne_k',
src    └──────────────────────┘
typ    └──────────────────────┘
doc    └──────────────────────┘
txt    └──────────────────────┘
par    └──────────────────────┘
pid                    └──────┘
 56    have NE : (A M k ∩ A M k').nonempty, from ⟨x, h⟩,
src    └────────┘         └────────┘  └───┘  └┘ 
typ    └────────┘         └────────┘  └───┘  └┘ 
doc    └────────┘         └────────┘  └───┘  └┘ 
txt    └────────┘         └────────┘  └───┘  └┘ 
par    └────────┘         └────────┘  └───┘  └┘ 
pid    └─────┘└─┘         └───────┘  └───┘  └┘ 
 57    have E : A M k ∩ A M k' = ∅  := disjoint_disjointed' k k' k_ne_k',
src    └───────┘          └───┘                       
typ    └───────┘          └───┘                       
doc    └───────┘          └───┘                       
txt    └───────┘          └───┘                       
par    └───────┘          └───┘                       
pid    └────┘└─┘          └───┘                       
 58    exact NE.ne_empty E,
src    └────┘           
typ    └────┘           
doc    └────┘           
txt    └────┘           
par    └────┘           
pid                    
 59  end,
 60  have x_mem_Union_k : ∀ {N x}, (x ∈ ⋃ M ≤ N, ⋃ k ≤ N, A M k) → x ∈ ⋃ k ≤ N, A (M N x) k :=
id                                                               
src                                                                    
typ                                                              
doc                                                                      
 61    λ N x h,
id         
typ        
 62      @nat.find_greatest_spec (λ M, x ∈ ⋃ k ≤ N, (A M k)) _ N (
id        └────────────────────┘                     
src       └────────────────────┘                
typ       └────────────────────┘                     
doc                                              
 63        let ⟨M, hM⟩ := mem_Union.1 (h) in
id         └─┘    └┘     └───────┘   
src                       └───────┘
typ        └─┘    └┘     └───────┘   
 64        let ⟨hM₁, hM₂⟩ := mem_Union.1 hM in
id         └─┘  └─┘  └─┘     └───────┘
src                          └───────┘
typ        └─┘  └─┘  └─┘     └───────┘
 65          ⟨M, ⟨hM₁, hM₂⟩⟩),
 66  have x_mem_A : ∀ {N x}, (x ∈ ⋃ M ≤ N, ⋃ k ≤ N, A M k) → x ∈ A (M N x) (k N x) :=
id                                                       
src                                                       
typ                                                      
doc                                            
 67    λ N x h,
id         
typ        
 68      @nat.find_greatest_spec (λ k, x ∈ A (M N x) k) _ N (
id        └────────────────────┘                  
src       └────────────────────┘         
typ       └────────────────────┘                  
 69        let ⟨k, hk⟩ := mem_Union.1 (x_mem_Union_k h) in
id         └─┘    └┘     └───────┘   └───────────┘ 
src                       └───────┘
typ        └─┘    └┘     └───────┘   └───────────┘ 
 70        let ⟨hk₁, hk₂⟩ := mem_Union.1 hk in
id         └─┘  └─┘  └─┘     └───────┘
src                          └───────┘
typ        └─┘  └─┘  └─┘     └───────┘
 71          ⟨k, ⟨hk₁, hk₂⟩⟩),
 72  have x_mem_A' : ∀ {N x}, (x ∈ ⋃ M ≤ N, ⋃ k ≤ N, A M k) → x ∈ A' (M N x) (k N x) :=
id                                               └┘         
src                                                        
typ                                              └┘         
doc                                             
 73    λ N x h, mem_of_subset_of_mem (inter_subset_left _ _) (x_mem_A h),
id           └──────────────────┘  └───────────────┘       └─────┘ 
src             └──────────────────┘  └───────────────┘
typ          └──────────────────┘  └───────────────┘       └─────┘ 
 74  -- prove that for all N, (F N) has finite range
 75  have F_finite : ∀ {N}, finite (range (F N)) :=
id                         └────┘  └───┘   
src                         └────┘  └───┘
typ                        └────┘  └───┘   
doc                         └────┘  └───┘
 76  begin
st   └─────
 77    assume N, apply finite_range_ite,
id                     └──────────────┘
src    └──────┘  └────┘└──────────────┘
typ    └──────┘  └────┘└──────────────┘
doc    └──────┘  └────┘
txt    └──────┘  └────┘
par    └──────┘  └────┘
pid    └──────┘       
st   ─────────┘└──────────────────────┘└─
 78    { rw range_comp, apply finite_image, exact finite_range_find_greatest },
id          └────────┘        └──────────┘        └────────────────────────┘
src      └─┘└────────┘  └────┘└──────────┘  └────┘└────────────────────────┘
typ      └─┘└────────┘  └────┘└──────────┘  └────┘└────────────────────────┘
doc      └─┘            └────┘              └────┘                          
txt      └─┘            └────┘              └────┘                          
par      └─┘            └────┘              └────┘                          
pid                                                                      
st   ───┘└───────────┘└──────────────────┘└─────────────────────────────────┘└┘
 79    { exact finite_range_const }
id             └────────────────┘
src      └────┘└────────────────┘
typ      └────┘└────────────────┘
doc      └────┘                  
txt      └────┘                  
par      └────┘                  
pid                             
st   ────────────────────────────┘└─
 80  end,
st   ──┘
 81  -- prove that for all N, (F N) is a measurable function
 82  have F_measurable : ∀ {N}, measurable (F N) :=
id                             └────────┘   
src                             └────────┘
typ                            └────────┘   
doc                             └────────┘
 83  begin
st   └─────
 84    assume N, refine measurable.if _ _ measurable_const,
id                      └───────────┘     └──────────────┘
src    └──────┘  └─────┘└───────────┘└───┘└──────────────┘
typ    └──────┘  └─────┘└───────────┘└───┘└──────────────┘
doc    └──────┘  └─────┘             └───┘
txt    └──────┘  └─────┘             └───┘
par    └──────┘  └─────┘             └───┘
pid    └──────┘                     └───┘
st   ─────────┘└─────────────────────────────────────────┘└─
 85    -- show `is_measurable {a : α | a ∈ ⋃ (M : ℕ) (H : M ≤ N) (k : ℕ) (H : k ≤ N), A M k}`
st   ─────────────────────────────────────────────────────────────────────────────────────────
 86    { rw set_of_mem_eq, simp [is_measurable.Union, is_measurable.Union_Prop, is_measurable_A] },
id          └───────────┘        └─────────────────┘  └──────────────────────┘
src      └─┘└───────────┘  └────┘└─────────────────┘└┘└──────────────────────┘└┘               └┘
typ      └─┘└───────────┘  └────┘└─────────────────┘└┘└──────────────────────┘└┘└─────────────┘└┘
doc      └─┘               └────┘                   └┘                        └┘               └┘
txt      └─┘               └────┘                   └┘                        └┘               └┘
par      └─┘               └────┘                   └┘                        └┘               └┘
pid                                              └┘                        └┘               
st   ───┘└──────────────┘└──────────────────────────────────────────────────────────────────────┘└┘
 87    -- show `measurable (λ (x : α), e (k N x))`
st   ──────────────────────────────────────────────
 88    apply measurable.comp measurable_from_nat, apply measurable_find_greatest,
id           └─────────────┘ └─────────────────┘        └──────────────────────┘
src    └────┘└─────────────┘└─────────────────┘  └────┘└──────────────────────┘
typ    └────┘└─────────────┘└─────────────────┘  └────┘└──────────────────────┘
doc    └────┘                                    └────┘
txt    └────┘                                    └────┘
par    └────┘                                    └────┘
pid                                                  
st   ──────────────────────────────────────────┘└──────────────────────────────┘└─
 89    assume k' k'_le_N, by_cases k'_eq_0 : k' = 0,
id                                           └┘
src    └───────────────┘  └───────┘       └─┘   └┘
typ    └───────────────┘  └───────┘       └─┘└┘ └┘
doc    └───────────────┘  └───────┘       └─┘   └┘
txt    └───────────────┘  └───────┘       └─┘   └┘
par    └───────────────┘  └───────┘       └─┘   └┘
pid    └───────────────┘                 └─┘   
st   ──────────────────┘└─────────────────────────┘└─
 90    -- if k' = 0
st   ───────────────
 91    have : {x | k N x = 0} = (-⋃ (M : ℕ) (H : M ≤ N) (k : ℕ) (H : k ≤ N), A M k) ∪
id                                                                            
src    └─────┘└──┘    └──┘  └────┘ └─────┘  └─────┘ └─────┘      └┘
typ    └─────┘└──┘   └──┘  └────┘ └─────┘  └─────┘ └─────┘      └┘
doc    └─────┘ └──┘    └──┘   └────┘ └─────┘   └─────┘ └─────┘      └┘ 
txt    └─────┘ └──┘    └──┘    └────┘ └─────┘   └─────┘ └─────┘       └┘ 
par    └─────┘ └──┘    └──┘    └────┘ └─────┘   └─────┘ └─────┘       └┘ 
pid    └───┘└┘ └──┘    └──┘    └────┘ └─────┘   └─────┘ └─────┘       └┘ 
st   ─────────────────────────────────────────────────────────────────────────────────
 92                      (⋃ (m ≤ N), A m 0 - ⋃ m' (hmm' : m < m') (hm'N : m' ≤ N) (k ≤ N), A m' k),
id                                                                                     
src  ───────────────────┘  └────┘    └─┘ └──────────┘   └────────┘    └─────┘      
typ  ───────────────────┘  └────┘    └─┘ └──────────┘   └────────┘   └─────┘    
doc  ───────────────────┘  └────┘    └─┘  └──────────┘    └────────┘    └─────┘      
txt  ───────────────────┘  └────┘    └─┘  └──────────┘    └────────┘    └─────┘      
par  ───────────────────┘  └────┘    └─┘  └──────────┘    └────────┘    └─────┘      
pid  ───────────────────┘  └────┘    └─┘  └──────────┘    └────────┘    └─────┘      
st   ────────────────────────────────────────────────────────────────────────────────────────────┘└─
 93    { ext, split,
src      └─┘  └───┘
typ      └─┘  └───┘
doc      └─┘  └───┘
txt      └─┘  └───┘
par      └─┘  └───┘
st   ───┘└─┘└─────┘└─
 94      { rw [mem_set_of_eq, mem_union_eq, or_iff_not_imp_left, mem_compl_eq, not_not_mem],
id             └───────────┘  └──────────┘  └─────────────────┘  └──────────┘  └─────────┘
src        └──┘└───────────┘└┘└──────────┘└┘└─────────────────┘└┘└──────────┘└┘└─────────┘
typ        └──┘└───────────┘└┘└──────────┘└┘└─────────────────┘└┘└──────────┘└┘└─────────┘
doc        └──┘             └┘            └┘                   └┘            └┘           
txt        └──┘             └┘            └┘                   └┘            └┘           
par        └──┘             └┘            └┘                   └┘            └┘           
pid          └┘             └┘            └┘                   └┘            └┘           
st   ─────┘└───────────────┘└────────────┘└───────────────────┘└────────────┘└───────────┘└──
 95        assume k_eq_0 x_mem,
src        └─────────────────┘
typ        └─────────────────┘
doc        └─────────────────┘
txt        └─────────────────┘
par        └─────────────────┘
pid        └─────────────────┘
st   ────────────────────────┘└─
 96        simp only [not_exists, exists_prop, mem_Union, not_and, sub_eq_diff, mem_diff],
id                    └────────┘  └─────────┘  └───────┘  └─────┘  └─────────┘  └──────┘
src        └─────────┘└────────┘└┘└─────────┘└┘└───────┘└┘└─────┘└┘└─────────┘└┘└──────┘
typ        └─────────┘└────────┘└┘└─────────┘└┘└───────┘└┘└─────┘└┘└─────────┘└┘└──────┘
doc        └─────────┘          └┘           └┘         └┘       └┘           └┘        
txt        └─────────┘          └┘           └┘         └┘       └┘           └┘        
par        └─────────┘          └┘           └┘         └┘       └┘           └┘        
pid            └──┘└┘          └┘           └┘         └┘       └┘           └┘        
st   ───────────────────────────────────────────────────────────────────────────────────┘└─
 97        refine ⟨M N x, ⟨nat.find_greatest_le, ⟨by { rw ← k_eq_0, exact x_mem_A x_mem} , _⟩⟩⟩,
id                      └──────────────────┘             └────┘        └─────┘ └───┘
src        └─────┘    └┘ └──────────────────┘└┘   └─┘└───┘      └┘└────┘            └──────┘
typ        └─────┘ └┘ └──────────────────┘└┘   └─┘└───┘└────┘└──────┘└─────┘└───┘└──────┘
doc        └─────┘    └┘                     └┘   └─┘└───┘      └┘└────┘            └──────┘
txt        └─────┘    └┘                     └┘   └─┘└───┘      └┘└────┘            └──────┘
par        └─────┘    └┘                     └┘   └─┘└───┘      └──────┘            └──────┘
pid                  └┘                     └┘   └──────┘      └──────┘            └──────┘
st   ──────────────────────────────────────────────┘└────────────┘└───────────────────┘└─────┘└─
 98        assume m hMm hmN k k_le_N,
src        └───────────────────────┘
typ        └───────────────────────┘
doc        └───────────────────────┘
txt        └───────────────────────┘
par        └───────────────────────┘
pid        └───────────────────────┘
st   ──────────────────────────────┘└─
 99        have := nat.find_greatest_is_greatest _ m ⟨hMm, hmN⟩,
id                 └───────────────────────────┘     └─┘  └─┘
src        └──────┘└───────────────────────────┘└─┘     └┘   
typ        └──────┘└───────────────────────────┘└─┘ └─┘└┘└─┘
doc        └──────┘                             └─┘     └┘   
txt        └──────┘                             └─┘     └┘   
par        └──────┘                             └─┘     └┘   
pid        └───┘└─┘                             └─┘     └┘   
st   ─────────────────────────────────────────────────────────┘└─
100        { simp only [not_exists, exists_prop, mem_Union, not_and] at this, exact this k k_le_N },
id                      └────────┘  └─────────┘  └───────┘  └─────┘                 └──┘  └────┘
src          └─────────┘└────────┘└┘└─────────┘└┘└───────┘└┘└─────┘└───────┘  └────┘           
typ          └─────────┘└────────┘└┘└─────────┘└┘└───────┘└┘└─────┘└───────┘  └────┘└──┘└────┘
doc          └─────────┘          └┘           └┘         └┘       └───────┘  └────┘           
txt          └─────────┘          └┘           └┘         └┘       └───────┘  └────┘           
par          └─────────┘          └┘           └┘         └┘       └───────┘  └────┘           
pid              └──┘└┘          └┘           └┘         └┘       └─────┘                  
st   ───────┘└─────────────────────────────────────────────────────────────┘└────────────────────┘└┘
101        { exact ⟨M N x, ⟨nat.find_greatest_le, x_mem_Union_k x_mem⟩⟩ } },
id                       └──────────────────┘  └───────────┘ └───┘
src          └────┘    └┘ └──────────────────┘└┘                  └─┘
typ          └────┘ └┘ └──────────────────┘└┘└───────────┘└───┘└─┘
doc          └────┘    └┘                     └┘                  └─┘
txt          └────┘    └┘                     └┘                  └─┘
par          └────┘    └┘                     └┘                  └─┘
pid                   └┘                     └┘                  └┘
st   ──────────────────────────────────────────────────────────────────┘└──┘
102      { simp only [mem_set_of_eq, mem_union_eq, mem_compl_eq],
id                    └───────────┘  └──────────┘  └──────────┘
src        └─────────┘└───────────┘└┘└──────────┘└┘└──────────┘
typ        └─────────┘└───────────┘└┘└──────────┘└┘└──────────┘
doc        └─────────┘             └┘            └┘            
txt        └─────────┘             └┘            └┘            
par        └─────────┘             └┘            └┘            
pid            └──┘└┘             └┘            └┘            
st   ──────────────────────────────────────────────────────────┘└─
103        by_cases x_mem : (x ∉ ⋃ (M : ℕ) (H : M ≤ N) (k : ℕ) (H : k ≤ N), A M k),
id                                                                     
src        └───────┘     └─┘  └────┘ └─────┘   └─────┘ └─────┘      
typ        └───────┘     └─┘ └────┘ └─────┘   └─────┘ └─────┘    
doc        └───────┘     └─┘   └────┘ └─────┘   └─────┘ └─────┘      
txt        └───────┘     └─┘    └────┘ └─────┘   └─────┘ └─────┘       
par        └───────┘     └─┘    └────┘ └─────┘   └─────┘ └─────┘       
pid                     └─┘    └────┘ └─────┘   └─────┘ └─────┘       
st   ────────────────────────────────────────────────────────────────────────────┘└─
104        { intro, apply find_greatest_eq_zero, assume k k_le_N hx,
id                        └───────────────────┘
src          └───┘  └────┘└───────────────────┘  └────────────────┘
typ          └───┘  └────┘└───────────────────┘  └────────────────┘
doc          └───┘  └────┘                       └────────────────┘
txt          └───┘  └────┘                       └────────────────┘
par          └───┘  └────┘                       └────────────────┘
pid                                             └────────────────┘
st   ───────┘└───┘└───────────────────────────┘└──────────────────┘└─
105          have : x ∈ ⋃ (M : ℕ) (H : M ≤ N) (k : ℕ) (H : k ≤ N), A M k,
id                                                             
src          └─────┘  └────┘ └─────┘   └─────┘ └─────┘     
typ          └─────┘ └────┘ └─────┘   └─────┘ └─────┘   
doc          └─────┘  └────┘ └─────┘   └─────┘ └─────┘     
txt          └─────┘   └────┘ └─────┘   └─────┘ └─────┘      
par          └─────┘   └────┘ └─────┘   └─────┘ └─────┘      
pid          └───┘└┘   └────┘ └─────┘   └─────┘ └─────┘      
st   ──────────────┘└─────────────────────────────────────────────────┘└─
106            { rw [mem_Union], use M N x,
id                   └───────┘         
src              └──┘└───────┘  └──┘  
typ              └──┘└───────┘  └──┘
doc              └──┘           └──┘  
txt              └──┘           └──┘  
par              └──┘           └──┘  
pid                └┘                
st   ───────────┘└───────────┘└──────────┘└─
107              rw mem_Union, use nat.find_greatest_le,
id                  └───────┘      └──────────────────┘
src              └─┘└───────┘  └──┘└──────────────────┘
typ              └─┘└───────┘  └──┘└──────────────────┘
doc              └─┘           └──┘
txt              └─┘           └──┘
par              └─┘           └──┘
pid                              
st   ───────────────────────┘└────────────────────────┘└─
108              rw mem_Union, use k, rw mem_Union, use k_le_N, assumption },
id                  └───────┘           └───────┘      └────┘
src              └─┘└───────┘  └──┘   └─┘└───────┘  └──┘        └─────────┘
typ              └─┘└───────┘  └──┘  └─┘└───────┘  └──┘└────┘  └─────────┘
doc              └─┘           └──┘   └─┘           └──┘        └─────────┘
txt              └─┘           └──┘   └─┘           └──┘        └─────────┘
par              └─┘           └──┘   └─┘           └──┘        └─────────┘
pid                                                                   
st   ───────────────────────┘└─────┘└────────────┘└──────────┘└───────────┘└┘
109          contradiction },
src          └────────────┘
typ          └────────────┘
doc          └────────────┘
txt          └────────────┘
par          └────────────┘
pid                       
st   ─────────────────────┘└┘
110        { rw not_not_mem at x_mem, assume h, cases h, contradiction,
id              └─────────┘                           
src          └─┘└─────────┘└───────┘  └──────┘  └────┘   └───────────┘
typ          └─┘└─────────┘└───────┘  └──────┘  └────┘  └───────────┘
doc          └─┘           └───────┘  └──────┘  └────┘   └───────────┘
txt          └─┘           └───────┘  └──────┘  └────┘   └───────────┘
par          └─┘           └───────┘  └──────┘  └────┘   └───────────┘
pid                       └───────┘  └──────┘       
st   ──────────────────────────────┘└────────┘└───────┘└─────────────┘└─
111          simp only [not_exists, exists_prop, mem_Union, not_and, sub_eq_diff, mem_diff] at h,
id                      └────────┘  └─────────┘  └───────┘  └─────┘  └─────────┘  └──────┘
src          └─────────┘└────────┘└┘└─────────┘└┘└───────┘└┘└─────┘└┘└─────────┘└┘└──────┘└────┘
typ          └─────────┘└────────┘└┘└─────────┘└┘└───────┘└┘└─────┘└┘└─────────┘└┘└──────┘└────┘
doc          └─────────┘          └┘           └┘         └┘       └┘           └┘        └────┘
txt          └─────────┘          └┘           └┘         └┘       └┘           └┘        └────┘
par          └─────────┘          └┘           └┘         └┘       └┘           └┘        └────┘
pid              └──┘└┘          └┘           └┘         └┘       └┘           └┘        └──┘
st   ──────────────────────────────────────────────────────────────────────────────────────────┘└─
112          rcases h with ⟨m, ⟨m_le_N, ⟨hx, hm⟩⟩⟩,
id                  
src          └─────┘ └───────────────────────────┘
typ          └─────┘└───────────────────────────┘
doc          └─────┘ └───────────────────────────┘
txt          └─────┘ └───────────────────────────┘
par          └─────┘ └───────────────────────────┘
pid                 └───────────────────────────┘
st   ────────────────────────────────────────────┘└─
113          by_cases m_lt_M : m < M N x,
id                                  
src          └───────┘      └─┘    
typ          └───────┘      └─┘ 
doc          └───────┘      └─┘    
txt          └───────┘      └─┘    
par          └───────┘      └─┘    
pid                        └─┘    
st   ──────────────────────────────────┘└─
114          { have := hm (M N x) m_lt_M nat.find_greatest_le (k N x) nat.find_greatest_le,
id                     └┘        └────┘                           └──────────────────┘
src            └──────┘      └┘                              └┘└──────────────────┘
typ            └──────┘└┘   └┘└────┘                     └┘└──────────────────┘
doc            └──────┘      └┘                              └┘
txt            └──────┘      └┘                              └┘
par            └──────┘      └┘                              └┘
pid            └───┘└─┘      └┘                              └┘
st   ─────────┘└─────────────────────────────────────────────────────────────────────────┘└─
115            have := x_mem_A x_mem,
id                     └─────┘ └───┘
src            └──────┘       
typ            └──────┘└─────┘└───┘
doc            └──────┘       
txt            └──────┘       
par            └──────┘       
pid            └───┘└─┘       
st   ──────────────────────────────┘└─
116            contradiction },
src            └────────────┘
typ            └────────────┘
doc            └────────────┘
txt            └────────────┘
par            └────────────┘
pid                         
st   ───────────────────────┘└┘
117          rw not_lt at m_lt_M, by_cases m_gt_M : m > M N x,
id              └────┘                                  
src          └─┘└────┘└────────┘  └───────┘      └─┘   
typ          └─┘└────┘└────────┘  └───────┘      └─┘
doc          └─┘      └────────┘  └───────┘      └─┘    
txt          └─┘      └────────┘  └───────┘      └─┘    
par          └─┘      └────────┘  └───────┘      └─┘    
pid                  └────────┘                └─┘    
st   ──────────────────────────┘└───────────────────────────┘└─
118          { have := nat.find_greatest_is_greatest _ m ⟨m_gt_M, m_le_N⟩,
id                     └───────────────────────────┘     └────┘  └────┘
src            └──────┘└───────────────────────────┘└─┘        └┘      
typ            └──────┘└───────────────────────────┘└─┘ └────┘└┘└────┘
doc            └──────┘                             └─┘        └┘      
txt            └──────┘                             └─┘        └┘      
par            └──────┘                             └─┘        └┘      
pid            └───┘└─┘                             └─┘        └┘      
st   ─────────┘└────────────────────────────────────────────────────────┘└─
119            { have : x ∈ ⋃ k ≤ N, A m k,
id                                
src              └─────┘  └───┘   
typ              └─────┘ └───┘
doc              └─────┘  └───┘   
txt              └─────┘   └───┘    
par              └─────┘   └───┘    
pid              └───┘└┘   └───┘    
st   ───────────┘└───────────────────────┘└─
120              { rw mem_Union, use 0, rw mem_Union, use nat.zero_le N, exact hx },
id                    └───────┘            └───────┘                  
src                └─┘└───────┘  └───┘  └─┘└───────┘
typ                └─┘└───────┘  └───┘  └─┘└───────┘                  
doc                └─┘           └───┘  └─┘
txt                └─┘           └───┘  └─┘
par                └─┘           └───┘  └─┘
pid                                    
st   ─────────────┘└──────────┘└─────┘└────────────┘                             └┘
121              contradiction },
st                             └┘
122            { use m, split, exact m_le_N, rw mem_Union, use 0, rw mem_Union,
id                                  └────┘
typ                                 └────┘
123              use nat.zero_le _, exact hx } },
st                                           └──┘
124          rw not_lt at m_gt_M, have M_eq_m := le_antisymm m_lt_M m_gt_M,
125          rw ← k'_eq_0, exact k_unique ⟨x_mem_A x_mem, by { rw [k'_eq_0, M_eq_m], exact hx }⟩ } } },
st                                                                                            └┘ └────┘
126    -- end of `have`
127    rw [k'_eq_0, this], apply is_measurable.union,
128    { apply is_measurable.compl,
129      simp [is_measurable.Union, is_measurable.Union_Prop, is_measurable_A] },
st                                                                             └┘
130    { simp [is_measurable.Union, is_measurable.Union_Prop, is_measurable.diff, is_measurable_A] },
st                                                                                                 └┘
131    -- if k' ≠ 0
132    have : {x | k N x = k'} = ⋃(m ≤ N), A m k' - ⋃m' (hmm' : m < m') (hm'N : m' ≤ N) (k ≤ N), A m' k,
id                                          └┘    └┘                                     
typ                                         └┘    └┘                                     
133    { ext, split,
134      { rw [mem_set_of_eq],
135        assume k_eq_k',
136        have x_mem : x ∈ ⋃ (M : ℕ) (H : M ≤ N) (k : ℕ) (H : k ≤ N), A M k,
id                                                                   
typ                                                                  
137        { have := find_greatest_of_ne_zero k_eq_k' k'_eq_0,
138          simp only [mem_Union], use M N x, use nat.find_greatest_le, use k', use k'_le_N,
id                                                                         └┘
typ                                                                        └┘
139          assumption },
st                      └┘
140        simp only [not_exists, exists_prop, mem_Union, not_and, sub_eq_diff, mem_diff],
141        refine ⟨M N x, ⟨nat.find_greatest_le, ⟨by { rw ← k_eq_k', exact x_mem_A x_mem} , _⟩⟩⟩,
id                   
typ                  
st                                                                                      └┘
142        assume m hMm hmN k k_le_N,
143        have := nat.find_greatest_is_greatest _ m ⟨hMm, hmN⟩,
id                                                        └─┘
typ                                                       └─┘
144          { simp only [not_exists, exists_prop, mem_Union, not_and] at this, exact this k k_le_N },
id                                                                                          └────┘
typ                                                                                         └────┘
st                                                                                                  └┘
145        exact ⟨M N x, ⟨nat.find_greatest_le, x_mem_Union_k x_mem⟩⟩ },
id                  
typ                 
st                                                                    └┘
146      { simp only [mem_set_of_eq, mem_union_eq, mem_compl_eq], assume h,
147        have x_mem : x ∈ ⋃ (M : ℕ) (H : M ≤ N) (k : ℕ) (H : k ≤ N), A M k,
id                                                                   
typ                                                                  
148          { simp only [not_exists, exists_prop, mem_Union, not_and, sub_eq_diff, mem_diff] at h,
149            rcases h with ⟨m, ⟨hm, ⟨hx, _⟩⟩⟩,
150            simp only [mem_Union], use m, use hm, use k', use k'_le_N, assumption },
id                                                      └┘
typ                                                     └┘
st                                                                                   └┘
151        simp only [not_exists, exists_prop, mem_Union, not_and, sub_eq_diff, mem_diff] at h,
152        rcases h with ⟨m, ⟨m_le_N, ⟨hx, hm⟩⟩⟩,
153        by_cases m_lt_M : m < M N x,
id                                
typ                               
154        { have := hm (M N x) m_lt_M nat.find_greatest_le (k N x) nat.find_greatest_le,
id                                                            
typ                                                           
155          have := x_mem_A x_mem,
156          contradiction },
st                         └┘
157        rw not_lt at m_lt_M, by_cases m_gt_M : m > M N x,
id                                                     
typ                                                    
158        { have := nat.find_greatest_is_greatest _ m ⟨m_gt_M, m_le_N⟩,
id                                                             └────┘
typ                                                            └────┘
159          have : x ∈ ⋃ k ≤ N, A m k :=
id                             
typ                            
160            by { rw mem_Union, use k', rw mem_Union, use k'_le_N, exact hx },
id                                    └┘
typ                                   └┘
st                                                                            └┘
161          contradiction,
162          { use m, split, exact m_le_N, rw mem_Union, use k', rw mem_Union, use k'_le_N, exact hx }},
id                                └────┘                    └┘
typ                               └────┘                    └┘
st                                                                                                   └─┘
163        rw not_lt at m_gt_M, have M_eq_m := le_antisymm m_lt_M m_gt_M,
164        exact k_unique ⟨x_mem_A x_mem, by { rw M_eq_m, exact hx }⟩ } },
st                                                                 └┘ └──┘
165    -- end of `have`
166    rw this, simp [is_measurable.Union, is_measurable.Union_Prop, is_measurable.diff, is_measurable_A]
167  end,
st   └─┘
168  -- start of proof
169  ⟨λ N, ⟨F N, λ x, measurable.preimage F_measurable is_measurable_singleton, F_finite⟩,
id              
typ             
170  -- The pointwise convergence part of the theorem
171  λ x, ⟨metric.tendsto_at_top.2 $ λ ε hε, classical.by_cases
id                                    
typ                                   
172  --first case : f x = 0
173  ( assume fx_eq_0 : f x = 0,
id                       
typ                      
174    have x_not_mem_A' : ∀ {M k}, x ∉ A' M k := λ M k,
id                                   └┘         
typ                                  └┘         
175    begin
176      simp only [mem_preimage, fx_eq_0, metric.mem_ball, one_div_eq_inv, norm_zero,
177                 not_and, not_lt, add_comm, not_le, dist_zero_right, mem_diff],
178      assume h, rw add_comm, exact inv_pos_of_nat
179    end,
st     └─┘
180    have x_not_mem_A  : ∀ {M k}, x ∉ A M k :=
id                                     
typ                                    
181      by { assume M k h, have := disjointed_subset h, exact absurd this x_not_mem_A' },
st                                                                                      └┘
182    have F_eq_0 : ∀ {N}, F N x = 0 := λ N, by simp [F, if_neg, mem_Union, x_not_mem_A],
id                                                
typ                                               
183    -- end of `have`
184    ⟨0, λ n hn, show dist (F n x) (f x) < ε, by {rw [fx_eq_0, F_eq_0, dist_self], exact hε}⟩ )
id                                     
typ                                    
st                                                                                           └┘
185  --second case : f x ≠ 0
186  ( assume fx_ne_0 : f x ≠ 0,
id                       
typ                      
187    let ⟨N₀, hN⟩ := exists_nat_one_div_lt (lt_min ((norm_pos_iff _).2 fx_ne_0) hε) in
id          └┘
typ         └┘
188    have norm_fx_gt : _ := (lt_min_iff.1 hN).1,
189    have ε_gt : _ := (lt_min_iff.1 hN).2,
190    have x_mem_Union_k_N₀ : x ∈ ⋃ k, A N₀ k :=
id                                        
typ                                       
191      let ⟨k, hk⟩ := mem_closure_range_iff_nat.1 (by { rw E_dense, exact mem_univ (f x) }) N₀ in
id                                                                                     
typ                                                                                    
st                                                                                         └┘
192      begin
193        rw [Union_disjointed, mem_Union], use k,
id                                               
typ                                              
194        rw [mem_preimage], simp, rw [← one_div_eq_inv, add_comm],
195        exact ⟨hk , le_of_lt norm_fx_gt⟩
196      end,
st       └─┘
197    let ⟨k₀, x_mem_A⟩ := mem_Union.1 x_mem_Union_k_N₀ in
id          └┘
typ         └┘
198    let n := max N₀ k₀ in
id         
typ        
199    have x_mem_Union_Union : ∀ {N} (hN : n ≤ N), x ∈ ⋃ M ≤ N, ⋃ k ≤ N, A M k := assume N hN,
id                                                                              └┘
typ                                                                             └┘
200      mem_Union.2
201        ⟨N₀, mem_Union.2
202          ⟨le_trans (le_max_left _ _) hN, mem_Union.2
id                                       └┘
typ                                      └┘
203            ⟨k₀, mem_Union.2 ⟨le_trans (le_max_right _ _) hN, x_mem_A⟩⟩⟩⟩,
id                                                           └┘
typ                                                          └┘
204    have FN_eq : ∀ {N} (hN : n ≤ N), F N x = e (k N x) := assume N hN, if_pos $ x_mem_Union_Union hN,
id                                                         └┘                             └┘
typ                                                        └┘                             └┘
205    -- start of proof
206    ⟨n, assume N hN,
id               
typ              
207    have N₀_le_N : N₀ ≤ N := le_trans (le_max_left _ _) hN,
id                         
typ                        
208    have k₀_le_N : k₀ ≤ N := le_trans (le_max_right _ _) hN,
id                         
typ                        
209    show dist (F N x) (f x) < ε, from
id                          
typ                         
210    calc
211      dist (F N x) (f x) = dist (e (k N x)) (f x) : by rw FN_eq hN
id                                       
typ                                      
212      ... < 1 / ((M N x : ℝ) + 1) :
id                         
src                          
typ                        
213      begin
214        have := x_mem_A' (x_mem_Union_Union hN),
215        rw [mem_preimage, mem_diff, metric.mem_ball, dist_comm] at this, exact this.1
216      end
st       └─┘
217      ... ≤ 1 / ((N₀ : ℝ) + 1)  :
id                        
src                       
typ                       
218      @one_div_le_one_div_of_le _ _  ((N₀ : ℝ) + 1) ((M N x : ℝ) + 1) (nat.cast_add_one_pos N₀)
id                                                           
src                                                             
typ                                                          
219      (add_le_add_right (nat.cast_le.2 (nat.le_find_greatest N₀_le_N
id                                                              └─────┘
typ                                                             └─────┘
220      begin rw mem_Union, use k₀, rw mem_Union, use k₀_le_N, exact x_mem_A end)) 1)
id                               └┘
typ                              └┘
st                                                                            └─┘
221      ... < ε : ε_gt ⟩ ),
id             
typ            
222  -- second part of the theorem
223  assume N, show ∥F N x∥ ≤ ∥f x∥ + ∥f x∥, from
id                                
typ                               
224  classical.by_cases
225  ( assume h : x ∈ ⋃ M ≤ N, ⋃ k ≤ N, A M k,
id                                   
typ                                  
226    calc
227      ∥F N x∥ = dist (F N x) 0 : by simp
id                       
typ                      
228      ... = dist (e (k N x)) 0 : begin simp only [F], rw if_pos h end
id                                                
typ                                               
st                                                                   └─┘
229      ... ≤ dist (e (k N x)) (f x) + dist (f x) 0 : dist_triangle _ _ _
id                                        
typ                                       
230      ... = dist (e (k N x)) (f x) + ∥f x∥ : by simp
id                                   
typ                                  
231      ... ≤ 1 / ((M N x : ℝ) + 1) + ∥f x∥ :
id                                    
src                          
typ                                   
232        le_of_lt $ add_lt_add_right (dist_ek_fx (x_mem_A h)) _
233      ... ≤ ∥f x∥ + ∥f x∥ : add_le_add_right (norm_fx (x_mem_A h) ) _)
id                     
typ                    
234  ( assume h : x ∉ ⋃ M ≤ N, ⋃ k ≤ N, A M k,
id                                   
typ                                  
235    have F_eq_0 : F N x = 0 := if_neg h,
id                     
typ                    
236    by { simp only [F_eq_0, norm_zero], exact add_nonneg (norm_nonneg _) (norm_nonneg _) } )⟩⟩
st                                                                                          └┘
237  
238  lemma simple_func_sequence_tendsto' {f : α → β} (hfm : measurable f)
id                                                                   
typ                                                                  
239    (hfi : integrable f) : ∃ (F : ℕ → (α →ₛ β)), (∀n, integrable (F n)) ∧
id                                                                   
src                                                                       
typ                                                                  
240     tendsto (λ n, ∫⁻ x,  nndist (F n x) (f x)) at_top  (𝓝 0) :=
id                                         
typ                                        
241  let ⟨F, hF⟩ := simple_func_sequence_tendsto hfm in
242  let G : ℕ → α → ennreal := λn x, nndist (F n x) (f x) in
id                └─────┘                       
src                 └─────┘
typ               └─────┘                       
doc                  └─────┘
243  let g : α → ennreal := λx, nnnorm (f x) + nnnorm (f x) + nnnorm (f x) in
id               └─┘ └┘                                            
src              └─┘ └┘
typ              └─┘ └┘                                            
doc              └─┘ └┘
244  have hF_meas : ∀ n, measurable (G n) := λ n, measurable.comp measurable_coe $
id                                          
typ                                         
245    (F n).measurable.nndist hfm,
id        
typ       
246  have hg_meas : measurable g := measurable.comp measurable_coe $ measurable.add
id                             
typ                            
247    (measurable.add hfm.nnnorm hfm.nnnorm) hfm.nnnorm,
248  have h_bound : ∀ n, ∀ₘ x, G n x ≤ g x := λ n, all_ae_of_all $ λ x, coe_le_coe.2 $
id                                                           
typ                                                          
249    calc
250      nndist (F n x) (f x) ≤ nndist (F n x) 0 + nndist 0 (f x) : nndist_triangle _ _ _
id                                                      
typ                                                     
251      ... = nnnorm (F n x) + nnnorm (f x) : by simp [nndist_eq_nnnorm]
id                                     
typ                                    
252      ... ≤ nnnorm (f x) + nnnorm (f x) + nnnorm (f x) : by { simp [nnreal.coe_le.symm, (hF x).2] },
id                                                                                       
typ                                                                                      
st                                                                                                   └┘
253  have h_finite : lintegral g < ⊤ :=
id                             
typ                            
254    calc
255      (∫⁻ x, nnnorm (f x) + nnnorm (f x) + nnnorm (f x)) =
id                                                
typ                                               
256        (∫⁻ x, nnnorm (f x)) + (∫⁻ x, nnnorm (f x)) + (∫⁻ x, nnnorm (f x)) :
id                                                                
typ                                                               
257      by rw [lintegral_add, lintegral_add]; simp only [measurable.coe_nnnorm hfm, measurable.add]
258      ... < ⊤ : by { simp only [and_self, add_lt_top], exact hfi},
st                                                                 └┘
259  have h_lim : ∀ₘ x, tendsto (λ n, G n x) at_top (𝓝 0) := all_ae_of_all $ λ x,
id                                                                        
typ                                                                       
260    begin
261      apply (@tendsto_coe ℕ at_top (λ n, nndist (F n x) (f x)) 0).2,
id                                                          
typ                                                         
262      apply (@nnreal.tendsto_coe ℕ at_top (λ n, nndist (F n x) (f x)) 0).1,
id                                                                 
typ                                                                
263      apply tendsto_iff_dist_tendsto_zero.1 (hF x).1
id                                                 
typ                                                
264    end,
st     └─┘
265  begin
266    use F, split,
267    { assume n, exact
268      calc
269        (∫⁻ a, nnnorm (F n a)) ≤ ∫⁻ a, nnnorm (f a) + nnnorm (f a) :
id                                   
typ                                  
270          lintegral_le_lintegral _ _
271            (by { assume a, simp only [coe_add.symm, coe_le_coe], exact (hF a).2 n })
id                                                                                 
typ                                                                                
st                                                                                    └┘
272         ... = (∫⁻ a, nnnorm (f a)) + (∫⁻ a, nnnorm (f a)) :
id                                          
typ                                         
273           lintegral_add (measurable.coe_nnnorm hfm) (measurable.coe_nnnorm hfm)
274         ... < ⊤ : by simp only [add_lt_top, and_self]; exact hfi },
st                                                                   └┘
275    convert @tendsto_lintegral_of_dominated_convergence _ _ G (λ a, 0) g
id                                                                      
typ                                                                     
276                hF_meas h_bound h_finite h_lim,
277    simp only [lintegral_zero]
278  end
st   └─┘
279  
280  end measure_theory